Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		f(g(i(a,b,b'),c),d)	→ if(e,f(b . c,d'),f(b' . c,d'))
2:		f(g(h(a,b),c),d)	→ if(e,f(b . g(h(a,b),c),d),f(c,d'))

There are 4 dependency pairs:


3:		F(g(i(a,b,b'),c),d)	→ F(b . c,d')
4:		F(g(i(a,b,b'),c),d)	→ F(b' . c,d')
5:		F(g(h(a,b),c),d)	→ F(b . g(h(a,b),c),d)
6:		F(g(h(a,b),c),d)	→ F(c,d')

The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 4, 2006